M, A:MsgA, k:Knd, l:IdLnk, tfL:(tg:Id(A.stateA.da(k)(A.dout(l,tg) List))) List.
M.rframe(A.sends tfL of k on l)  Prop 

latex

Definitions

M.rframe(A.sends tfL of k on l), M.state, M.da(a), (s1  s2 mod x), M.dout(l,tg), M.ds(x), MsgA, State(ds), xdom(f). v=f(x)   P(x;v), x,y. t(x;y), P  Q, left+right, deq-member(eq;x;L), Prop, s = t, 1of(t), f(a), 2of(t), l[i], b, x  dom(f), #$n, {i..j}, {x:A| B(x) }, , AB, A, False, P  Q, a<b, i  j < k, P & Q, ||as||, a:A fp B(a), x:AB(x), Id, IdDeq, x:AB(x), Top, type List, f(x)?z, x. t(x), x.A(x), KindDeq, rcv(l,tg), x:A. B(x), Type, Void, IdLnk, t  T, Knd

Lemmas

Knd wf, IdLnk wf, rcv wf, Kind-deq wf, fpf-cap wf, top wf, id-deq wf, Id wf, fpf-trivial-subtype-top, length wf1, fpf-dom wf, assert wf, select wf, pi2 wf, pi1 wf, int seg wf, not wf, deq-member wf, fpf-all wf, msga wf